COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Notes on Heavy Duty Set Theory
C00013 ENDMK
C⊗;
Notes on Heavy Duty Set Theory


	"Heavy Duty Set Theory" (abbreviated HDST) is to be an
FOL axiomatization of set theory suitable for proving theorems
in various domains of mathematics, MTC, and artificial intelligence.
The object of the axiomatization is to make proofs as short as
possible and to get as close as possible to informal notation.
Therefore, it will have a large number of axioms.

Recommendations:

1. HDST will be like Kelley's system in containing both classes
and sets and also axiom schemata for comprehension and replacement.

2. There will be members of sets that are not sets, and the axioms
will have to be adjusted for this.  Numbers and S-expressions
will be sorts and will be axiomatized and identified with the
machine versions.
This may be incompatible with identifying numbers with certain sets.
An isomorphism with this set can be asserted if wanted.
Presumably the building the integers from the null set is useful in
the theory of ordinal numbers, since it identifies the ordering with
set inclusion and drastically reduces the number of kinds of entities
occurring in proofs.

3. apply(f,x) giving the value of f(x) will be present and suitably
axiomatized.  In order that apply can be a function in the logic
we will need an INDCONST UU which is the nominal value for undefined
quantities. *****I'm not quite sure of this.***** 1979 That's right,
but it would be well to be able to write f(x) for this.  Functions
of several arguments give notational problems.

4. Suitable sorts for sets, classes, and objects will be set up.

5. Can we make cons and the ordered pair former synonymous?
If we want the ordered tuple to satisfy reasonable axioms,
it should be made more like LISP.
For example, we should distinguish between ordered pairs
and tuples: Suppose we use (x.y) for the ordered pair
usually denoted by <x,y>.  We will then use λ for
the 0-tuple, and define the n+1-tuple by suitable instances of
<x1,x2,...,xn> = (x1.<x2,...,xn>).

6. We will distinguish two systems; those that don't involve modifications
to FOL and those that do.

7. If we can modify FOL, then the finite set former {a,b,d,e} should
be such that membership and subset relationships are immediate.
Thus "SET-OBVIOUSITY {b {d e}} ⊂ {{f d} a b} 7;", where 7 is f=e,
should work.  Richard points out that a collection of such results
can be obtained from taut by a suitable translation.

8. For ordered lists, inclusion relations should be obvious.
In general: what set-theoretic relations are obvious?

Here is an attempt to modify kelley.ax[ax,rww] to suit.  The current
version her reads into FOL.  The SETINDUCTION axiom is not correct.
Ordered triples have been omitted pending a notation change.  ⊗ and
EXP2 and EXP3 have been omitted.

This file is HEAVY.SET[W76,JMC] and a set of axioms is HEAVY.AX[W76,JMC].